Require Import RocqOfRust.RocqOfRust.
Require Import RocqOfRust.links.M.
Require Import plonky3.commit_539bbc84.blake3_air.constants.

(* 
pub const BITS_PER_LIMB: usize = 16;
pub const U32_LIMBS: usize = 32 / BITS_PER_LIMB;
*)
Definition BITS_PER_LIMB : Usize.t := {|
  Integer.value := 16;
|}.
Definition U32_LIMBS : Usize.t := {|
  Integer.value := 2;
|}.
